T:Type, L:T List, P:(||L||Prop).
(x:||L||. Dec(P(x)))  (i:||L||. P(i))  (i:||L||. P(i) & (j:||L||. i<j  P(j))) 

latex

Definitions	x:A. B(x), P & Q, t  T, P  Q, x:A. B(x), Prop, ||as||, {i..j}, Dec(P), A, ij, False, AB, i  j < k, S  T, S  T, , True, T, {T}, interleaving_occurence(T;L1;L2;L;f1;f2), P  Q, SQType(T)
Lemmas	decidable lt, increasing implies, le wf, not wf, decidable wf, int seg wf, length wf1, interleaving split